Inference at * 1 
Iof proof for Lemma mul bounds 1a:



1. a : 
2. b : 
  0  (a * b) 

latex

 by Assert (a * 0)  (a * b) 

latex

 1: .....assertion..... NILNIL

 1:   (a * 0)  (a * b)
 2: 

 2: 3. (a * 0)  (a * b)
 2:   0  (a * b)
 .

Definitions

A  B, #$n, n * m